/* copied verbatim from purecss.io. it is to change fonts of the whole app. DO NOT MESS WITH IT. */
body, html, button, input, select, textarea, .pure-g [class *= "pure-u"] {
   font-family: 'Ubuntu';
}

/* signature styling for all single page web apps */
html, body {
   width: 100%;
   height: 100%;
}
div {
   -webkit-box-sizing: border-box;
   -moz-box-sizing: border-box;
   box-sizing: border-box;
}

/* styling of the editor */
.CodeMirror {
   font-family: 'Ubuntu Mono';
   height: inherit;
}


/* all other styling */
.mine-full-height { height: 100%; }
.mine-scrollable { overflow: auto; }
.mine-centered { text-align: center; }
.mine-middle { position: absolute; top: 50%; margin-top: -0.5em; }
.mine-padded { padding: 2%; }
.mine-hover { cursor: pointer; }
.mine-horizontal-flow { white-space: nowrap; }
.mine-relative { position: relative; }
.mine-button { font-size: smaller; }

#main-area { height: 97%; border-bottom: thin solid black; }
#status-bar { height: 3%; border-top: thin solid black; }

#editor { border-left: thin solid black; }
#navigator { border-right: thin solid black; }

#buttons { height: 6%; }
#location { height: 4%; }
#listing { height: 90%; }

#back-button { color: olive; }
#path { font-weight: bold; }

.list { margin-top: 4.5%; margin-bottom: 4.5%; }
.entry { margin-top: 1.5%; margin-bottom: 1.5%; }
